YES 13.187 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ IFR

mainModule Main
  ((showsPrec :: Int  ->  Bool  ->  [Char]  ->  [Char]) :: Int  ->  Bool  ->  [Char]  ->  [Char])

module Main where
  import qualified Prelude


If Reductions:
The following If expression
if b then (showChar '(') . p . showChar ')' else p

is transformed to
showParen0 p True = (showChar '(') . p . showChar ')'
showParen0 p False = p



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR

mainModule Main
  ((showsPrec :: Int  ->  Bool  ->  [Char]  ->  [Char]) :: Int  ->  Bool  ->  [Char]  ->  [Char])

module Main where
  import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR

mainModule Main
  ((showsPrec :: Int  ->  Bool  ->  [Char]  ->  [Char]) :: Int  ->  Bool  ->  [Char]  ->  [Char])

module Main where
  import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ NumRed

mainModule Main
  ((showsPrec :: Int  ->  Bool  ->  [Char]  ->  [Char]) :: Int  ->  Bool  ->  [Char]  ->  [Char])

module Main where
  import qualified Prelude


Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ NumRed
                ↳ HASKELL
                  ↳ Narrow

mainModule Main
  (showsPrec :: Int  ->  Bool  ->  [Char]  ->  [Char])

module Main where
  import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ NumRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(vx560, vx561), vx59) → new_psPs(vx561, vx59)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ NumRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_showParen0(vx55, vx56, Succ(vx57000), Succ(vx580), vx59) → new_showParen0(vx55, vx56, vx57000, vx580, vx59)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: